googologywikiaorg-20200223-history
User blog:Rpakr/A Formal Definition of Pair Sequence System using BM1 Rules
Introduction In this blog post, I will define BM1 pair sequences formally without using things like ... which are ambiguous, and defines BM1 number. Definitions In this section I will define some functions, sets, etc. I will be using in the definition. When I use quotation marks, it means the string inside them should be treated as strings and not as numbers or expressions. Nonnegative integer \(\mathbb{N}_0\) is the set of all nonnegative integer. \(\mathbb{N}_0=\mathbb{N}\cup\{0\}\) Concatenation of two strings When A and B are strings, \(con(A,B)\) is defined to be the string that is the concatenation of A and B. Pair function Define \(Pair(a,b)\) to be the string “(a,b)” when \(a\) and \(b\) are nonnegative integers. \(Pair(a,b)=P\Leftrightarrow (a\in\mathbb{N}_0∧b\in\mathbb{N}_0∧P=con(“(“,con(a,con(”,”,con(b,”)”)))))\) Pair \(Pair(A,B)\) is a pair when \(A\in\mathbb{N}_0\) and \(B\in\mathbb{N}_0\). The set of all pairs is called Pair. \(P\in Pair\Leftrightarrow\exists A\exists B(P=Pair(A,B))\) First number Define \(First(P)\) to be the first number of the pair when \(P\) is a pair. When \(P\) is not a pair, \(First(P)\) is undefined. \(First(P)=A\Leftrightarrow \exists B(P=Pair(A,B))\) Second number Define \(Second(P)\) to be the second number of the pair when \(P\) is a pair. When \(P\) is not a pair, \(Second(P)\) is undefined. \(Second(P)=B\Leftrightarrow \exists A(P=Pair(A,B))\) Adding a number to a pair Define \(P+a\) to be the sequence that adds a to the first term of \(P\). \(P+a=Q\Leftrightarrow (P\in Pair\wedge a\in\mathbb{N}_0\wedge Q=Pair(First(P)+a,Second(P)))\) Sequence Define sequence recursively. A pair is a sequence. If \(A\) is a pair and \(B\) is a sequence, \(con(A,B)\) is a sequence. \(Seq\) is the set of all sequences. \(S\in Seq\Leftrightarrow (S\in Pair\vee (S=con(A,B)\wedge A\in Pair\wedge B\in Seq))\) Expression function Define \(Exp(S,n)\) to be the string “Sn” when \(S\) is a sequence and \(n\in\mathbb{N}\). \(Exp(S,n)=P\Leftrightarrow (S\in Seq\wedge n\in N\wedge P=con(S,con(”“,con(n,””))))\) Expression \(Exp(S,n)\) is an expression when \(S\) is a sequence and \(n\in\mathbb{N}\). The set of all expressions is called \(Exp\). \(E\in Exp\Leftrightarrow\exists S\exists n(E=Exp(S,n))\) Sequence function Define \(Seq(E)\) to be the sequence of expression \(E\). \(Seq(E)=S\Leftrightarrow\exists n(E=Exp(S,n))\) Bracket function Define \(Bracket(E)\) to be the number inside the bracket of expression \(E\). \(Bracket(E)=n\Leftrightarrow\exists S(E=Exp(S,n))\) Length Define length recursively. If a sequence is a pair, its length is 1. If a sequence can be written as \(con(A,B)\) when \(A\) is a pair and \(B\) is a sequence, its length is the the length of \(B\) plus one. \(Len(S)\) means the length of sequence \(S\). \(Len(S)=1\Leftrightarrow S\in Pair\) \(Len(S)=n+1\Leftrightarrow\exists A\in Pair(\exists B\in Seq(S=con(A,B)\wedge Len(B)=n))\) nth pair \(GetPair(n,S)\) is the \(n\)th pair of \(S\). \(S\in Pair\Rightarrow (GetPair(1,S)=S)\) \(S\notin Pair\Rightarrow (GetPair(1,S)=P\Leftrightarrow\exists S_2\in Seq(S=con(P,S_2)\wedge P\in Pair))\) \(\exists P\in Pair(S=con(P,S_2))\Rightarrow (GetPair(n+1,S)=GetPair(n,S_2))\) m pairs from nth pair \(GetPair(n,m,S)\) is the sequence which is \(m\) pairs from the \(n\)th pair of \(S\). \(GetPair(n,0,S) is empty string\) \(GetPair(n,1,S)=GetPair(n,S)\) \(n+m1\Rightarrow(Del(S)=S_2\Leftrightarrow\exists P\in Pair(con(S_2,P)=S))\) Adding a number to a sequence \(AddSeq(n,S)\) is sequence \(S\) with \(n\) added in the first number. \(P(n,S,0)=S\) \(P(n,S,k+1)=con(P(n,S,k),GetPair(Len(P(n,S,k))-Len(S)+1,P(n,S,k))+n)\) \(AddSeq(n,S)=P(n,S,n)\) Adding a number to a sequence and repeat \(AddSeqCon(S,d,r)\) is sequence \(S\), repeated \(r\) times and for each repetition the first number increases by \(d\). \(AddSeqCon(S,d,1)=S\) \(r\in N\Rightarrow (AddSeqCon(S,d,r+1)=con(AddSeqCon(S,d,r1),AddSeq(r(d-1),S)))\) Definition of BM1 pair sequences Base case \((E\in Exp\wedge Len(Seq(E))=1\wedge First(GetPair(1,Seq(E)))=0\wedge Second(GetPair(1,Seq(E)))=0)\Rightarrow Eval(E)=Bracket(E)+1\) Successor case \((E\in Exp\wedge Len(Seq(E))>1\wedge First(GetPair(Len(Seq(E)),Seq(E)))=0\wedge Second(GetPair(Len(Seq(E)),Seq(E)))=0)\Rightarrow Eval(E)=Exp(Del(Seq(E)),Bracket(E)+1)\) Limit case Define LimExp. \(E\in LimExp\Leftrightarrow (E\in Exp\wedge Len(Seq(E))>1\wedge First(GetPair(Len(Seq(E)),Seq(E)))>0)\) Bad root ∀R((E∈LimExp∧First(GetPair(R,Seq(E)))0)∨(D=0∧Second(GetPair(Len(Seq(E)),Seq(E)))=0))⇔Delta(E)=D) Good Part Good(E)=GetPair(1,BR(E)-1,Seq(E)) Bad Part Bad(E)=GetPair(BR(E),Len(E)-BR(E),Seq(E)) Value Eval(E)=Exp(con(Good(E),AddSeqCon(Bad(E),Delta(E),Bracket(E))),Bracket(E)) Value of BM expression Eval(E)∈N⇒Val(E)=Eval(E) Eval(E)∉N⇒Val(E)=Val(Eval(E)) Definition of BM1 number f(n)=Eval(Exp(“(0,0)(1,1)(2,1)(3,1)”,n)) BM1 number=f^10(10) Category:Blog posts